$\forall$$T$:Type. finite{-}type($T$) $\in$ Type